/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2003  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: AbstractUniqueTable.java,v 1.4 2004/06/03 03:54:03 fqian Exp $
package SableJBDD.bdd.internal;

import SableJBDD.bdd.*;
import SableJBDD.bdd.util.*;
import SableJBDD.cache.CacheProfiler;

/**
 * A unique table is a canonical mapping from a triple key (var, low, high)
 * to a BDD internal node.
 *
 * @author Feng Qian
 */
public abstract class AbstractUniqueTable extends CacheProfiler implements UniqueTable {
  // element for hash table, for internal use only 
  interface Element {
    boolean isEmpty();
    JBddNode getNode();
    Element getNext();
    void setNext(Element next);
  }

  // a list of entries 
  protected Element[]  entries;

  /**
   * Defines a unique table with a specific number of entries.
   */
  AbstractUniqueTable(int size) {
    this.entries = new Element[size];
  }
  
  private long totalallocations = 0;
  
  /**
   * Finds or creates a BddNode by a triple key.
   * @param var the BDD variable
   * @param low the false branch
   * @param high the true branch
   * @return the canonical bdd node
   */
  public synchronized JBddNode findOrCreate(JBddVariable var, 
                                            JBddNode low, 
                                            JBddNode high) {
    assert var != null;
    assert low != null;
    assert high != null;
   
    int hash = HashFunction.hash(var.hashCode(), low.hashCode(), high.hashCode());

    int idx = hash % this.entries.length;

    Element prev = null;
    Element el = this.entries[idx];
    JBddNode node = null;
    
    if (PROFILING) step();

    while (el != null) {
      
      // prune the list by removing dead soft reference object
      if (el.isEmpty()) {
        if (prev == null) {
          this.entries[idx] = el.getNext();
        } else {
          prev.setNext(el.getNext());
        }
      } else {
        JBddNode tmpnode = el.getNode();
        if (tmpnode != null && tmpnode.matches(var, low, high)) {
          node = tmpnode;
          break;
        }
        prev = el;               // advance prev 
      }
    
      if (PROFILING) step();
      el = el.getNext();
    }

    if (node == null) { // did not find it, create one
      this.totalallocations ++;
      node = makeNode(var, low, high);
      this.entries[idx]   = newElement(node, this.entries[idx]);
      if (PROFILING) miss();
    } else {
      if (PROFILING) hit();
    }

    return node;
  }

  protected abstract Element newElement(JBddNode node, Element next);
  protected abstract JBddNode makeNode(JBddVariable var, JBddNode low, JBddNode high);
}
